Error handling cleanup in src/util (files starting with a-g) #2762

danpoe · 2018-08-20T11:52:41Z

No description provided.

kroening · 2018-08-20T19:50:29Z

A key problem of throwing exceptions is that they can't be used for warnings.

Thus, I'd recommend retaining the message handlers in places where warnings might be needed.

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 700b28e).
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

tautschnig · 2018-09-05T19:43:41Z

src/util/array_name.cpp

-    if(expr.operands().size()!=2)
-      throw "index takes two operands";
+    DATA_INVARIANT(
+      expr.operands().size() == 2, "index expression has two operands");


Use to_index_expr and let it do all the error checking and reporting.

tautschnig · 2018-09-05T19:43:55Z

src/util/array_name.cpp

@@ -44,7 +45,8 @@ std::string array_name(
  }
  else if(expr.id()==ID_member)
  {
-    assert(expr.operands().size()==1);
+    DATA_INVARIANT(
+      expr.operands().size() == 1, "member expression has one operand");


to_member_expr

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 23e9de7).
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

allredj

This PR failed Diffblue compatibility checks (cbmc commit: b0bab14).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84005870
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

allredj

Passed Diffblue compatibility checks (cbmc commit: b0bab14).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84005870

hannes-steffenhagen-diffblue · 2018-09-14T12:30:41Z

src/util/exception_utils.h

+  std::string reason;
+
+public:
+  system_exceptiont(const std::string &reason) : reason(reason)


Should be marked as explicit, should take reason as plain string rather than reference and should move reason.

hannes-steffenhagen-diffblue · 2018-09-14T12:30:56Z

src/util/exception_utils.h

+public:
+  system_exceptiont(const std::string &reason) : reason(reason)
+  {
+  }


Should go into exception_utils.cpp

hannes-steffenhagen-diffblue · 2018-09-14T12:31:14Z

src/util/exception_utils.h

+    res += "System Exception\n";
+    res += "Reason: " + reason + "\n";
+    return res;
+  }


Should go into exception_utils.cpp

hannes-steffenhagen-diffblue · 2018-09-14T12:31:50Z

src/util/parse_options.cpp

@@ -76,6 +76,12 @@ int parse_options_baset::main()
    std::cerr << e.what() << "\n";
    return CPROVER_EXIT_USAGE_ERROR;
  }
+  catch(system_exceptiont &e)


We should probably add a base class like cprover_exceptiont so we don't have to do this for every single kind of exception we introduce.

allredj

This PR failed Diffblue compatibility checks (cbmc commit: e0715f3).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85464121
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

tautschnig · 2018-09-21T13:03:18Z

src/util/graph.h

@@ -787,7 +789,7 @@ void grapht<N>::tarjan(tarjant &t, node_indext v) const
  {
    while(true)
    {
-      assert(!t.scc_stack.empty());
+      INVARIANT(!t.scc_stack.empty(), "");


Missing error message

tautschnig · 2018-09-21T13:03:29Z

src/util/graph.h

@@ -536,12 +537,13 @@ void grapht<N>::disconnect_unreachable(const std::vector<node_indext> &src)
  std::size_t reachable_idx = 0;
  for(std::size_t i = 0; i < nodes.size(); i++)
  {
+    INVARIANT(
+      reachable_idx >= reachable.size() || i <= reachable[reachable_idx], "");


Missing message

allredj

Passed Diffblue compatibility checks (cbmc commit: 73a215c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85731119

peterschrammel · 2018-09-24T21:20:05Z

src/linking/static_lifetime_init.cpp

-        rhs=zero_initializer(symbol.type, symbol.location, ns, message_handler);
-        assert(rhs.is_not_nil());
-      }
-      catch(...)


tautschnig

Needs another rebase and several nit-picks, plus an actual concern about static_lifetime_init.

tautschnig · 2018-09-25T06:21:00Z

src/util/config.cpp

@@ -1069,21 +1095,17 @@ static irep_idt string_from_ns(
  const irep_idt id=CPROVER_PREFIX "architecture_"+what;
  const symbolt *symbol;

-  if(ns.lookup(id, symbol))
-    throw "failed to find "+id2string(id);
+  bool not_found = ns.lookup(id, symbol);


Nit pick: const

tautschnig · 2018-09-25T06:21:09Z

src/util/config.cpp

@@ -1095,21 +1117,24 @@ static unsigned unsigned_from_ns(
  const irep_idt id=CPROVER_PREFIX "architecture_"+what;
  const symbolt *symbol;

-  if(ns.lookup(id, symbol))
-    throw "failed to find "+id2string(id);
+  bool not_found = ns.lookup(id, symbol);


Nit pick: const

tautschnig · 2018-09-25T06:21:27Z

src/util/config.cpp

-  if(to_integer(to_constant_expr(tmp), int_value))
-    throw
-      "failed to convert symbol table configuration entry `"+id2string(id)+"'";
+  bool error = to_integer(to_constant_expr(tmp), int_value);


Nit pick: const

tautschnig · 2018-09-25T06:23:22Z

src/linking/static_lifetime_init.cpp

-      {
-        return true;
-      }
+      namespacet ns(symbol_table);


tautschnig · 2018-09-25T06:25:43Z

src/ansi-c/ansi_c_entry_point.cpp

@@ -177,8 +177,7 @@ bool ansi_c_entry_point(
    return false; // give up
  }

-  if(static_lifetime_init(symbol_table, symbol.location, message_handler))
-    return true;
+  static_lifetime_init(symbol_table, symbol.location, message_handler);


This procedure still has a non-void return type, should that change?

Ok, changed it to void. The remaining check in static_lifetime_init is a precondition now.

…h a-g

allredj

Passed Diffblue compatibility checks (cbmc commit: 756c0b9).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85854252

danpoe requested review from kroening, peterschrammel, pkesseli, smowton and tautschnig as code owners August 20, 2018 11:52

danpoe force-pushed the refactor/error-handling-util branch from af53c84 to 1fa7178 Compare August 20, 2018 11:54

danpoe requested review from cesaro, cristina-david, mgudemann, NathanJPhillips and thk123 as code owners August 20, 2018 14:11

danpoe force-pushed the refactor/error-handling-util branch 2 times, most recently from e69d31c to 700b28e Compare September 5, 2018 14:07

allredj reviewed Sep 5, 2018

View reviewed changes

tautschnig reviewed Sep 5, 2018

View reviewed changes

danpoe force-pushed the refactor/error-handling-util branch from 700b28e to 23e9de7 Compare September 6, 2018 13:06

danpoe requested a review from chrisr-diffblue as a code owner September 6, 2018 13:06

danpoe force-pushed the refactor/error-handling-util branch from 23e9de7 to b0bab14 Compare September 6, 2018 13:08

allredj reviewed Sep 6, 2018

View reviewed changes

hannes-steffenhagen-diffblue reviewed Sep 14, 2018

View reviewed changes

danpoe force-pushed the refactor/error-handling-util branch from b0bab14 to e0715f3 Compare September 20, 2018 16:44

allredj reviewed Sep 20, 2018

View reviewed changes

tautschnig reviewed Sep 21, 2018

View reviewed changes

danpoe force-pushed the refactor/error-handling-util branch from e0715f3 to ffc52fb Compare September 21, 2018 16:50

tautschnig assigned danpoe Sep 24, 2018

tautschnig added the Needs rebase label Sep 24, 2018

danpoe force-pushed the refactor/error-handling-util branch from ffc52fb to 73a215c Compare September 24, 2018 12:35

danpoe removed the Needs rebase label Sep 24, 2018

allredj reviewed Sep 24, 2018

View reviewed changes

peterschrammel approved these changes Sep 24, 2018

View reviewed changes

tautschnig added the Needs rebase label Sep 25, 2018

tautschnig reviewed Sep 25, 2018

View reviewed changes

danpoe added 2 commits September 25, 2018 11:30

Error handling cleanup in src/util, for files with names starting wit…

d5535a9

…h a-g

Error handling cleanup in expr_initializer.cpp (and implied changes)

756c0b9

danpoe force-pushed the refactor/error-handling-util branch from 73a215c to 756c0b9 Compare September 25, 2018 10:58

danpoe removed the Needs rebase label Sep 25, 2018

allredj reviewed Sep 25, 2018

View reviewed changes

tautschnig approved these changes Sep 25, 2018

View reviewed changes

tautschnig merged commit 5b5ba13 into diffblue:develop Sep 25, 2018

danpoe deleted the refactor/error-handling-util branch June 2, 2020 17:13

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Error handling cleanup in src/util (files starting with a-g) #2762

Error handling cleanup in src/util (files starting with a-g) #2762

danpoe commented Aug 20, 2018 •

edited

Loading

kroening commented Aug 20, 2018

allredj left a comment

tautschnig Sep 5, 2018

tautschnig Sep 5, 2018

allredj left a comment

allredj left a comment

allredj left a comment

hannes-steffenhagen-diffblue Sep 14, 2018

hannes-steffenhagen-diffblue Sep 14, 2018

hannes-steffenhagen-diffblue Sep 14, 2018

hannes-steffenhagen-diffblue Sep 14, 2018

allredj left a comment

tautschnig Sep 21, 2018

tautschnig Sep 21, 2018

allredj left a comment

peterschrammel Sep 24, 2018

tautschnig left a comment

tautschnig Sep 25, 2018

tautschnig Sep 25, 2018

tautschnig Sep 25, 2018

tautschnig Sep 25, 2018

tautschnig Sep 25, 2018

danpoe Sep 25, 2018

allredj left a comment

Error handling cleanup in src/util (files starting with a-g) #2762

Error handling cleanup in src/util (files starting with a-g) #2762

Conversation

danpoe commented Aug 20, 2018 • edited Loading

kroening commented Aug 20, 2018

allredj left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tautschnig left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

danpoe commented Aug 20, 2018 •

edited

Loading